h1: A Taste of the Bitter Lesson in Automated Theorem Proving
自动化定理证明中的苦涩教训：简单 Agent 循环
🧭 Agent 自反思 + 形式化验证
FAIR at Meta · EPFL · CERMICS, ENPC, Institut Polytechnique de Paris · New York University
提出 h1，一个只靠高效 Lean 接口与验证反馈自反思的简单 agent 循环，在形式定理证明达到 SOTA 并追上复杂工作流
📌 工作参考价值（4 点）
- 构建 LLM agent 做 query 生成、推荐文案或策略搜索时，不要先上规划/多智能体分解；先用单 agent + 可执行验证器（搜索 API 结果、商品约束、SQL 执行）做自反思循环，用 pass@1/多采样衡量，效率和效果常超复杂编排。
- 工具/环境接口的反馈延迟与信息质量是关键：把验证器返回做成结构化、可增量复用（如错误位置、候选修正），减少模型盲目重试；类比 h1 的 Lean 4 增量编译与错误上下文。
- 做消融和 matched-model 对比：换更强模型或更多计算会混淆 workflow 收益；固定模型，对比简单 loop vs 复杂 agent 架构，避免苦涩教训。
- 如果业务里有可靠执行环境（规则校验、线上仿真、评分器），把计算预算花在多次验证反馈循环（test-time compute）上，可能比重构提示/工作流更划算。